COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	must[w87,jmc]		must and might as well
C00004 ENDMK
C⊗;
must[w87,jmc]		must and might as well

	Extending the blocks world axiomatization to consider sequences
of actions or even strategies suggests formalizing the concepts
 {\it must} and {\it might as well}.  If we have
%
$$on(A,B) ∧ on(B,C) ∧ on(C,D),$$
%
then in order to move block $D$, we {\it must} first move $A$,
and if $A$ is to go on $C$ eventually we {\it might as well}
first move $A$ to the table.

	The following should be a theorem:
%
$$∀a s x y l.loc(y,s)=top(x) ∧ loc(x,s) ≠ l ∧ loc(x,result(a,s)) = l
	⊃ ∃l↓1.member(move(y,l↓1),a).$$
%

We can write it with a predicate $must$ as follows:
%
$$∀s x y l.loc(y,s)=top\ x ∧ loc(x,s) ≠ l
	⊃ must(λl↓1.move(y,l↓1),λs'.loc(x,s') = l,s).$$

	It looks like we need to be able to say that we must move
$y$ somewhere.  This requires a quantified expression as an argument
for $must$.  It is another reason for figuring out how to handle
quantified expressions as concept arguments in first order theories.